Nuprl Lemma : qmul-ident-div
11,40
postcript
pdf
r
,
s
:
. (
(
r
= 0
))
(((
r
/
r
) *
s
) =
s
)
latex
Definitions
P
&
Q
,
T
,
P
Q
,
P
Q
,
True
,
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
qmul
one
qrng
,
qdiv-self
,
true
wf
,
squash
wf
,
qmul
wf
,
int
inc
rationals
,
rationals
wf
,
not
wf
origin
r, s:
. (
(r = 0 
)) 
(((r/r) * s) = s) r, s:. ((r = 0 )) (((r/r) * s) = s) 
T
Q Q
T Qx:A. B(x)
T